(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 6) (_ BitVec 15)) (_ BitVec 4))
(declare-fun f1 ( (_ BitVec 15)) (_ BitVec 13))
(declare-fun p0 ( (_ BitVec 10)) Bool)
(declare-fun p1 ( (_ BitVec 4)) Bool)
(declare-fun v0 () (_ BitVec 15))
(declare-fun v1 () (_ BitVec 7))
(declare-fun v2 () (_ BitVec 6))
(declare-fun v3 () (_ BitVec 6))
(declare-fun v4 () (_ BitVec 5))
(assert (let ((e5(_ bv2311 14)))
(let ((e6(_ bv3 2)))
(let ((e7 (ite (bvule v0 ((_ sign_extend 13) e6)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (ite (bvuge ((_ zero_extend 3) e6) v4) (_ bv1 1) (_ bv0 1))))
(let ((e9 (ite (bvult e6 ((_ zero_extend 1) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e10 (f0 v2 ((_ zero_extend 14) e9))))
(let ((e11 (ite (p1 ((_ extract 6 3) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (bvmul v0 ((_ sign_extend 9) v2))))
(let ((e13 (bvadd ((_ zero_extend 14) e8) v0)))
(let ((e14 (f1 ((_ zero_extend 10) v4))))
(let ((e15 (ite (bvslt ((_ sign_extend 2) e6) e10) (_ bv1 1) (_ bv0 1))))
(let ((e16 (ite (p1 ((_ extract 5 2) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e17 (concat e11 v1)))
(let ((e18 (bvmul e13 e12)))
(let ((e19 (ite (p1 ((_ extract 11 8) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e20 ((_ rotate_right 2) e10)))
(let ((e21 (ite (p1 e20) (_ bv1 1) (_ bv0 1))))
(let ((e22 (bvand ((_ zero_extend 8) v1) e13)))
(let ((e23 (ite (bvsgt ((_ sign_extend 5) e11) v2) (_ bv1 1) (_ bv0 1))))
(let ((e24 (ite (p0 ((_ zero_extend 4) v3)) (_ bv1 1) (_ bv0 1))))
(let ((e25 ((_ rotate_left 2) e22)))
(let ((e26 (bvxnor e21 e8)))
(let ((e27 ((_ rotate_left 0) e6)))
(let ((e28 (bvxnor v2 ((_ zero_extend 5) e19))))
(let ((e29 (bvor e21 e15)))
(let ((e30 ((_ repeat 2) v3)))
(let ((e31 (bvxor ((_ zero_extend 8) v2) e5)))
(let ((e32 (p1 ((_ zero_extend 2) e27))))
(let ((e33 (p0 ((_ sign_extend 9) e19))))
(let ((e34 (bvsgt ((_ zero_extend 13) e7) e5)))
(let ((e35 (bvuge e27 ((_ zero_extend 1) e15))))
(let ((e36 (bvsle e31 ((_ zero_extend 13) e19))))
(let ((e37 (bvsle e18 e18)))
(let ((e38 (bvult e23 e9)))
(let ((e39 (bvslt e24 e23)))
(let ((e40 (bvule e23 e11)))
(let ((e41 (p0 ((_ extract 14 5) e25))))
(let ((e42 (bvslt ((_ zero_extend 14) e8) e12)))
(let ((e43 (bvult ((_ sign_extend 8) e20) e30)))
(let ((e44 (bvsge v2 ((_ zero_extend 5) e26))))
(let ((e45 (distinct ((_ zero_extend 11) e10) v0)))
(let ((e46 (bvuge ((_ sign_extend 14) e24) e25)))
(let ((e47 (bvsle ((_ zero_extend 14) e9) e22)))
(let ((e48 (bvult e27 ((_ sign_extend 1) e26))))
(let ((e49 (bvugt e11 e29)))
(let ((e50 (= e28 ((_ sign_extend 5) e23))))
(let ((e51 (p1 ((_ extract 5 2) v3))))
(let ((e52 (bvsge ((_ zero_extend 3) e30) e25)))
(let ((e53 (bvsle ((_ zero_extend 1) e31) e25)))
(let ((e54 (bvugt e7 e24)))
(let ((e55 (bvuge e17 ((_ zero_extend 3) v4))))
(let ((e56 (p1 ((_ zero_extend 2) e27))))
(let ((e57 (distinct ((_ zero_extend 9) v2) e13)))
(let ((e58 (bvugt e6 ((_ sign_extend 1) e7))))
(let ((e59 (bvuge ((_ zero_extend 2) e27) e20)))
(let ((e60 (= e22 e13)))
(let ((e61 (bvsle e17 ((_ sign_extend 7) e7))))
(let ((e62 (bvuge e25 ((_ sign_extend 1) e5))))
(let ((e63 (bvsge e23 e8)))
(let ((e64 (bvult ((_ sign_extend 1) e19) e6)))
(let ((e65 (bvugt e5 ((_ sign_extend 13) e7))))
(let ((e66 (distinct e27 ((_ sign_extend 1) e24))))
(let ((e67 (bvsle e17 ((_ zero_extend 7) e15))))
(let ((e68 (bvsge ((_ sign_extend 9) v2) e18)))
(let ((e69 (bvult v3 ((_ sign_extend 5) e24))))
(let ((e70 (bvsle ((_ sign_extend 2) e6) e20)))
(let ((e71 (bvule e10 ((_ zero_extend 3) e21))))
(let ((e72 (bvsle ((_ sign_extend 5) e23) v2)))
(let ((e73 (bvsle v3 ((_ sign_extend 5) e8))))
(let ((e74 (p1 ((_ sign_extend 3) e21))))
(let ((e75 (bvsle ((_ zero_extend 6) e28) e30)))
(let ((e76 (bvuge ((_ sign_extend 5) e21) v3)))
(let ((e77 (bvsle ((_ zero_extend 1) e28) v1)))
(let ((e78 (bvsle e10 ((_ zero_extend 3) e16))))
(let ((e79 (bvuge ((_ zero_extend 4) e9) v4)))
(let ((e80 (bvult e30 ((_ sign_extend 8) e10))))
(let ((e81 (bvsgt ((_ sign_extend 13) e6) e12)))
(let ((e82 (p1 ((_ extract 6 3) v1))))
(let ((e83 (bvuge e13 ((_ sign_extend 14) e11))))
(let ((e84 (bvuge e13 ((_ sign_extend 14) e7))))
(let ((e85 (= v0 e25)))
(let ((e86 (bvsle e18 ((_ sign_extend 10) v4))))
(let ((e87 (bvult e14 ((_ sign_extend 9) e10))))
(let ((e88 (not e40)))
(let ((e89 (ite e55 e88 e43)))
(let ((e90 (not e80)))
(let ((e91 (xor e67 e84)))
(let ((e92 (xor e45 e57)))
(let ((e93 (or e76 e82)))
(let ((e94 (ite e78 e70 e74)))
(let ((e95 (=> e36 e86)))
(let ((e96 (or e92 e65)))
(let ((e97 (and e53 e91)))
(let ((e98 (xor e83 e58)))
(let ((e99 (=> e51 e54)))
(let ((e100 (=> e32 e66)))
(let ((e101 (and e85 e97)))
(let ((e102 (ite e46 e33 e64)))
(let ((e103 (or e42 e38)))
(let ((e104 (not e73)))
(let ((e105 (xor e81 e77)))
(let ((e106 (= e62 e87)))
(let ((e107 (not e89)))
(let ((e108 (= e69 e61)))
(let ((e109 (xor e104 e106)))
(let ((e110 (xor e98 e107)))
(let ((e111 (and e39 e103)))
(let ((e112 (= e96 e50)))
(let ((e113 (=> e93 e60)))
(let ((e114 (ite e37 e37 e109)))
(let ((e115 (and e101 e112)))
(let ((e116 (not e102)))
(let ((e117 (ite e75 e35 e47)))
(let ((e118 (=> e72 e116)))
(let ((e119 (not e111)))
(let ((e120 (ite e94 e119 e105)))
(let ((e121 (=> e113 e63)))
(let ((e122 (= e59 e68)))
(let ((e123 (or e110 e52)))
(let ((e124 (=> e118 e56)))
(let ((e125 (and e48 e95)))
(let ((e126 (not e120)))
(let ((e127 (not e99)))
(let ((e128 (and e34 e126)))
(let ((e129 (= e125 e123)))
(let ((e130 (or e108 e49)))
(let ((e131 (= e117 e121)))
(let ((e132 (ite e124 e114 e100)))
(let ((e133 (or e44 e41)))
(let ((e134 (ite e127 e129 e132)))
(let ((e135 (=> e134 e131)))
(let ((e136 (not e130)))
(let ((e137 (=> e133 e122)))
(let ((e138 (not e135)))
(let ((e139 (=> e90 e138)))
(let ((e140 (or e139 e79)))
(let ((e141 (ite e128 e115 e115)))
(let ((e142 (=> e140 e71)))
(let ((e143 (xor e142 e141)))
(let ((e144 (=> e143 e143)))
(let ((e145 (or e136 e137)))
(let ((e146 (= e144 e145)))
e146
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
